A System for Deduction-based Formal Verification of Workflow-oriented Software Models

摘要

The work concerns formal verification of workflow-oriented software modelsusing deductive approach. The formal correctness of a model's behaviour isconsidered. Manually building logical specifications, which are considered as aset of temporal logic formulas, seems to be the significant obstacle for aninexperienced user when applying the deductive approach. A system, and itsarchitecture, for the deduction-based verification of workflow-oriented modelsis proposed. The process of inference is based on the semantic tableaux methodwhich has some advantages when compared to traditional deduction strategies.The algorithm for an automatic generation of logical specifications isproposed. The generation procedure is based on the predefined workflow patternsfor BPMN, which is a standard and dominant notation for the modeling ofbusiness processes. The main idea for the approach is to consider patterns,defined in terms of temporal logic,as a kind of (logical) primitives whichenable the transformation of models to temporal logic formulas constituting alogical specification. Automation of the generation process is crucial forbridging the gap between intuitiveness of the deductive reasoning and thedifficulty of its practical application in the case when logical specificationsare built manually. This approach has gone some way towards supporting,hopefully enhancing our understanding of, the deduction-based formalverification of workflow-oriented models.